M:MsgA. M || M 

latex

Definitions	t  T, x:A. B(x), x. t(x), Id, Knd, type List, IdLnk, x.A(x), x:A  B(x), product-deq(A;B;a;b), a:A fp B(a), x:A.B(x), Top, Atom$n, strong-subtype(A;B), P  Q, x:AB(x), s = t, P  Q, P & Q, P  Q, KindDeq, IdDeq, Void, t.2, rcv(l,tg), f  g, <a, b>, True, T, f(a), x(s), EqDecider(T), f(x)?z, t.1, State(ds), Valtype(da;k), S  T, suptype(S; T), IdLnkDeq, , , f || g, M1 ||decl M2, MsgA, M1 || M2, Type
Lemmas	msga wf, id-deq wf, Kind-deq wf, Knd wf, deq wf, bool wf, squash wf, true wf, rationals wf, IdLnk wf, idlnk-deq wf, ma-valtype wf, fpf-join wf, pi1 wf, ma-state wf, top wf, fpf-cap wf, rcv wf, pi2 wf, fpf-join-idempotent, Id wf, fpf wf, fpf-trivial-subtype-top, subtype-fpf3, strong-subtype-self, product-deq wf, fpf-compatible-self